/*@ x>=0 && y>=0
 */
int f (int x, int y)
{
  int a, b;
  a = 0;
  b = x;
  while (b >= y)  /*@ a*y+b==x && b>=0 */
  {
    b = b-y;
    a = a+1;
  }
  return a;
}
/*@  result == x/y
 */


/*@ */
void main()
{
  int x;
  x = f (12, 3);
  print(x);
  return;
}
/*@ */
